<HTML><HEAD>
<META NAME="copyright" CONTENT="Copyright (c) 1986-2006, Eiffel Software and others">
<META NAME="license" CONTENT="Eiffel Forum License v2 (see forum.txt)">
<META NAME="description" CONTENT="To easily manage allocation and release of allocated C memory, and to perform insertion of basic elements. Byte order is by default platform specific. Although memory allocation routines do not accept a zero sized pointer MANAGED_POINTER does by allocating in fact a 1 byte sized pointer for this particular case.">
<META NAME="library" CONTENT="Free implementation of ELKS library">
<META NAME="keywords" CONTENT="Eiffel class">
<META NAME="keywords" CONTENT="Eiffel class">
<TITLE>managed_pointer Flat contracts</TITLE></HEAD>
<BODY BGCOLOR="white">
<P ALIGN="CENTER">Automatic generation produced by ISE Eiffel</P>
<PRE><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="managed_pointer_chart.html">Chart</A></TD><TD><A HREF="managed_pointer_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE><B>indexing</B>
    description: "[
        To easily manage allocation and release of allocated C memory, and
        to perform insertion of basic elements. Byte order is by default
        platform specific.
        Although memory allocation routines do not accept a zero sized pointer
        MANAGED_POINTER does by allocating in fact a 1 byte sized pointer for
        this particular case.
    ]"
    library: "Free implementation of ELKS library"
    copyright: "Copyright (c) 1986-2006, Eiffel Software and others"
    license: "Eiffel Forum License v2 (see forum.txt)"
    date: "$Date: 2008-05-24 02:24:07 +0200 (Sat, 24 May 2008) $"
    revision: "$Revision: 170 $"

<B>class</B> <B>interface</B>
    <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>


<B>create</B> 
    <A NAME="f_make"><A HREF="../base/managed_pointer_flatshort.html#f_make">make</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Allocate </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red"> with </FONT>`n'<FONT COLOR="red"> bytes.</FONT>
        <B>require</B>
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            item_set: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
            count_set: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = n
            is_shared_set: <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>
    <A NAME="f_make_from_array"><A HREF="../base/managed_pointer_flatshort.html#f_make_from_array">make_from_array</A> (data: <A HREF="../base/array_flatshort.html">ARRAY</A> [<A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Allocate </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red"> with </FONT>`data.count'<FONT COLOR="red"> bytes and copy</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> content of </FONT>`data'<FONT COLOR="red"> into </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red">.</FONT>
        <B>require</B>
            data_not_void: data /= <B>Void</B>
        <B>ensure</B>
            item_set: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
            count_set: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = data.<A HREF="../base/array_flatshort.html#f_count">count</A>
            is_shared_set: <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>
    <A NAME="f_make_from_pointer"><A HREF="../base/managed_pointer_flatshort.html#f_make_from_pointer">make_from_pointer</A> (a_ptr: <A HREF="../base/pointer_flatshort.html">POINTER</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy </FONT>`a_count'<FONT COLOR="red"> bytes from </FONT>`a_ptr'<FONT COLOR="red"> into current.</FONT>
        <B>require</B>
            a_ptr_not_null: a_ptr /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            item_set: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
            count_set: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = n
            is_shared_set: <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>
    <A NAME="f_share_from_pointer"><A HREF="../base/managed_pointer_flatshort.html#f_share_from_pointer">share_from_pointer</A> (a_ptr: <A HREF="../base/pointer_flatshort.html">POINTER</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Use directly </FONT>`a_ptr'<FONT COLOR="red"> with count </FONT>`n'<FONT COLOR="red"> to hold current data.</FONT>
        <B>require</B>
            a_ptr_valid: a_ptr = <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A> <B>implies</B> n = 0
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            item_set: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> = a_ptr
            count_set: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = n
            is_shared_set: <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access</FONT>

    <A NAME="f_count"><A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of elements that Current can hold.</FONT>

    <A NAME="f_generating_type"><A HREF="../base/any_flatshort.html#f_generating_type">generating_type</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generating_type_not_void: <B>Result</B> /= <B>Void</B>
            generating_type_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_generator"><A HREF="../base/any_flatshort.html#f_generator">generator</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating class</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (base class of the type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generator_not_void: <B>Result</B> /= <B>Void</B>
            generator_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_is_shared"><A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red"> shared with another memory area?</FONT>

    <A NAME="f_item"><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A>: <A HREF="../base/pointer_flatshort.html">POINTER</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access to allocated memory.</FONT>
    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Comparison</FONT>

    <A NAME="f_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> or attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some, other) <B>implies</B> <B>Result</B>
            both_or_none_void: (some = <B>Void</B>) <B>implies</B> (<B>Result</B> = (other = <B>Void</B>))
            same_type: (<B>Result</B> <B>and</B> (some /= <B>Void</B>)) <B>implies</B> (other /= <B>Void</B> <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other))
            symmetric: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (other, some)
</A>
    <A NAME="f_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_equal">equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to objects considered equal?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (other))
</A>
    <A NAME="f_is_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (other: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`Current'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (<B>Current</B>)
</A>
    <A NAME="f_is_equal"><A HREF="../base/managed_pointer_flatshort.html#f_is_equal">is_equal</A> (other: <B>like</B> <B>Current</B>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`other'<FONT COLOR="red"> attached to an object considered equal to current object?</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
            consistent: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
</A>
    <A NAME="f_standard_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached to</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> field-by-field identical objects of the same type?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default object comparison criterion.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other))
</A>
    <A NAME="f_standard_is_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`other'<FONT COLOR="red"> attached to an object of the same type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> as current object, and field-by-field identical to it?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Status report</FONT>

    <A NAME="f_conforms_to"><A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does type of current object conform to type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of </FONT>`other'<FONT COLOR="red"> (as per Eiffel: The Language, chapter 13)?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
</A>
    <A NAME="f_same_type"><A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is type of current object identical to type of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other) <B>and</B> other.<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>))
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Resizing</FONT>

    <A NAME="f_resize"><A HREF="../base/managed_pointer_flatshort.html#f_resize">resize</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reallocate </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red"> to hold </FONT>`n'<FONT COLOR="red"> bytes.</FONT>
        <B>require</B>
            n_non_negative: n &gt;= 0
            not_shared: <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Duplication</FONT>

    <A NAME="f_copy"><A HREF="../base/managed_pointer_flatshort.html#f_copy">copy</A> (other: <B>like</B> <B>Current</B>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Update current object using fields of object attached</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to </FONT>`other'<FONT COLOR="red">, so as to yield equal objects. If </FONT><A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> and current is not large enough to hold </FONT>`other'<FONT COLOR="red"> create</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> a new pointer area and </FONT><A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A><FONT COLOR="red"> is set to </FONT>`False'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_equal: <A HREF="../base/managed_pointer_flatshort.html#f_is_equal">is_equal</A> (other)
        <B>ensure then</B>
            sharing_status_not_preserved: (<B>old</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A> <B>and</B> <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>) <B>implies</B> (other.<A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> &gt; <B>old</B> <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>)
</A>
    <A NAME="f_deep_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_copy">deep_copy</A> (other: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Effect equivalent to that of:</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red">		</FONT><A HREF="../base/managed_pointer_flatshort.html#f_copy">copy</A><FONT COLOR="red"> (</FONT>`other'<FONT COLOR="red"> . </FONT><A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A><FONT COLOR="red">)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, other)
</A>
    <A NAME="f_deep_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A>: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object structure recursively duplicated from Current.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_twin_not_void: <B>Result</B> /= <B>Void</B>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, <B>Result</B>)
</A>
    <A NAME="f_standard_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_copy">standard_copy</A> (other: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy every field of </FONT>`other'<FONT COLOR="red"> onto corresponding field</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_standard_equal: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other)
</A>
    <A NAME="f_standard_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_twin">standard_twin</A>: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object field-by-field identical to </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default copying semantics.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            standard_twin_not_void: <B>Result</B> /= <B>Void</B>
            equal: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (<B>Result</B>, <B>Current</B>)
</A>
    <A NAME="f_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>: <A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object equal to </FONT>`Current'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT><A HREF="../base/any_flatshort.html#f_twin">twin</A><FONT COLOR="red"> calls </FONT><A HREF="../base/managed_pointer_flatshort.html#f_copy">copy</A><FONT COLOR="red">; to change copying/twining semantics, redefine </FONT><A HREF="../base/managed_pointer_flatshort.html#f_copy">copy</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            twin_not_void: <B>Result</B> /= <B>Void</B>
            is_equal: <B>Result</B>.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Basic operations</FONT>

    <A NAME="f_default"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default">default</A>: ?<A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of object's type</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_pointer"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>: <A HREF="../base/pointer_flatshort.html">POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of type </FONT>`POINTER'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Avoid the need to write </FONT>`p'<FONT COLOR="red">.</FONT><A HREF="../base/any_flatshort.html#f_default">default</A><FONT COLOR="red"> for</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> some </FONT>`p'<FONT COLOR="red"> of type </FONT>`POINTER'<FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_rescue"><A HREF="../base/any_flatshort.html#f_default_rescue">default_rescue</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Process exception for routines with no Rescue clause.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Default: do nothing.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_do_nothing"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_do_nothing">do_nothing</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Execute a null action.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access bits size</FONT>

    <A NAME="f_boolean_bits"><A HREF="../base/platform_flatshort.html#f_boolean_bits">boolean_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`BOOLEAN'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_character_32_bits"><A HREF="../base/platform_flatshort.html#f_character_32_bits">character_32_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`CHARACTER_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_character_8_bits"><A HREF="../base/platform_flatshort.html#f_character_8_bits">character_8_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`CHARACTER_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_16_bits"><A HREF="../base/platform_flatshort.html#f_integer_16_bits">integer_16_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`INTEGER_16'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_32_bits"><A HREF="../base/platform_flatshort.html#f_integer_32_bits">integer_32_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`INTEGER_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_64_bits"><A HREF="../base/platform_flatshort.html#f_integer_64_bits">integer_64_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`INTEGER_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_8_bits"><A HREF="../base/platform_flatshort.html#f_integer_8_bits">integer_8_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`INTEGER_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_16_bits"><A HREF="../base/platform_flatshort.html#f_natural_16_bits">natural_16_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`NATURAL_16'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_32_bits"><A HREF="../base/platform_flatshort.html#f_natural_32_bits">natural_32_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`NATURAL_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_64_bits"><A HREF="../base/platform_flatshort.html#f_natural_64_bits">natural_64_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`NATURAL_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_8_bits"><A HREF="../base/platform_flatshort.html#f_natural_8_bits">natural_8_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`NATURAL_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_pointer_bits"><A HREF="../base/platform_flatshort.html#f_pointer_bits">pointer_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`POINTER'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_real_32_bits"><A HREF="../base/platform_flatshort.html#f_real_32_bits">real_32_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`REAL_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_real_64_bits"><A HREF="../base/platform_flatshort.html#f_real_64_bits">real_64_bits</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bits in a value of type </FONT>`REAL_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access bytes size</FONT>

    <A NAME="f_boolean_bytes"><A HREF="../base/platform_flatshort.html#f_boolean_bytes">boolean_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`BOOLEAN'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_character_32_bytes"><A HREF="../base/platform_flatshort.html#f_character_32_bytes">character_32_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 4</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`CHARACTER_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_character_8_bytes"><A HREF="../base/platform_flatshort.html#f_character_8_bytes">character_8_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 1</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`CHARACTER_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_16_bytes"><A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 2</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`INTEGER_16'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_32_bytes"><A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 4</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`INTEGER_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_64_bytes"><A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`INTEGER_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_integer_8_bytes"><A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 1</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`INTEGER_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_16_bytes"><A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 2</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`NATURAL_16'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_32_bytes"><A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 4</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`NATURAL_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_64_bytes"><A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`NATURAL_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_natural_8_bytes"><A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 1</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`NATURAL_8'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_pointer_bytes"><A HREF="../base/platform_flatshort.html#f_pointer_bytes">pointer_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`POINTER'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_real_32_bytes"><A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 4</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`REAL_32'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>

    <A NAME="f_real_64_bytes"><A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of bytes in a value of type </FONT>`REAL_64'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access: Big-endian format</FONT>

    <A NAME="f_read_integer_16_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16_be">read_integer_16_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32_be">read_integer_32_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64_be">read_integer_64_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_8_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8_be">read_integer_8_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_16_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16_be">read_natural_16_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32_be">read_natural_32_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64_be">read_natural_64_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_8_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8_be">read_natural_8_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_32_be">read_real_32_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_32_flatshort.html">REAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_64_be">read_real_64_be</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_64_flatshort.html">REAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access: Little-endian format</FONT>

    <A NAME="f_read_integer_16_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16_le">read_integer_16_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32_le">read_integer_32_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64_le">read_integer_64_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_8_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8_le">read_integer_8_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_16_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16_le">read_natural_16_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32_le">read_natural_32_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64_le">read_natural_64_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_8_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8_le">read_natural_8_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_32_le">read_real_32_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_32_flatshort.html">REAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_64_le">read_real_64_le</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_64_flatshort.html">REAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access: Platform specific</FONT>

    <A NAME="f_read_array"><A HREF="../base/managed_pointer_flatshort.html#f_read_array">read_array</A> (pos, a_count: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/array_flatshort.html">ARRAY</A> [<A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read </FONT><A HREF="../base/managed_pointer_flatshort.html#f_count">count</A><FONT COLOR="red"> bytes at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            count_positive: a_count &gt; 0
            valid_position: (pos + a_count) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            read_array_not_void: <B>Result</B> /= <B>Void</B>
            read_array_valid_count: <B>Result</B>.<A HREF="../base/array_flatshort.html#f_count">count</A> = a_count
</A>
    <A NAME="f_read_boolean"><A HREF="../base/managed_pointer_flatshort.html#f_read_boolean">read_boolean</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read BOOLEAN at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_boolean_bytes">boolean_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_character"><A HREF="../base/managed_pointer_flatshort.html#f_read_character">read_character</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read CHARACTER at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_character_8_bytes">character_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_16"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16">read_integer_16</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_32"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32">read_integer_32</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_64"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64">read_integer_64</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_integer_8"><A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8">read_integer_8</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read INTEGER_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_16"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16">read_natural_16</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_16 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_32"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32">read_natural_32</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_64"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64">read_natural_64</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_natural_8"><A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8">read_natural_8</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read NATURAL_8 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_pointer"><A HREF="../base/managed_pointer_flatshort.html#f_read_pointer">read_pointer</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/pointer_flatshort.html">POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read POINTER at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_pointer_bytes">pointer_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_32"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_32">read_real_32</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_32_flatshort.html">REAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_32 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_read_real_64"><A HREF="../base/managed_pointer_flatshort.html#f_read_real_64">read_real_64</A> (pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/real_64_flatshort.html">REAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Read REAL_64 at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Concatenation</FONT>

    <A NAME="f_append"><A HREF="../base/managed_pointer_flatshort.html#f_append">append</A> (other: <B>like</B> <B>Current</B>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append </FONT>`other'<FONT COLOR="red"> at the end of Current.</FONT>
        <B>require</B>
            not_shared: <B>not</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
            other_not_void: other /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Element change: Big-endian format</FONT>

    <A NAME="f_put_integer_16_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_16_be">put_integer_16_be</A> (i: <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16_be">read_integer_16_be</A> (pos)
</A>
    <A NAME="f_put_integer_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_32_be">put_integer_32_be</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32_be">read_integer_32_be</A> (pos)
</A>
    <A NAME="f_put_integer_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_64_be">put_integer_64_be</A> (i: <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64_be">read_integer_64_be</A> (pos)
</A>
    <A NAME="f_put_integer_8_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_8_be">put_integer_8_be</A> (i: <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8_be">read_integer_8_be</A> (pos)
</A>
    <A NAME="f_put_natural_16_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_16_be">put_natural_16_be</A> (i: <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16_be">read_natural_16_be</A> (pos)
</A>
    <A NAME="f_put_natural_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_32_be">put_natural_32_be</A> (i: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32_be">read_natural_32_be</A> (pos)
</A>
    <A NAME="f_put_natural_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_64_be">put_natural_64_be</A> (i: <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64_be">read_natural_64_be</A> (pos)
</A>
    <A NAME="f_put_natural_8_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_8_be">put_natural_8_be</A> (i: <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8_be">read_natural_8_be</A> (pos)
</A>
    <A NAME="f_put_real_32_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_32_be">put_real_32_be</A> (v: <A HREF="../base/real_32_flatshort.html">REAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`v'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: v = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_32_be">read_real_32_be</A> (pos)
</A>
    <A NAME="f_put_real_64_be"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_64_be">put_real_64_be</A> (v: <A HREF="../base/real_64_flatshort.html">REAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`v'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in big-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: v = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_64_be">read_real_64_be</A> (pos)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Element change: Little-endian format</FONT>

    <A NAME="f_put_integer_16_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_16_le">put_integer_16_le</A> (i: <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16_le">read_integer_16_le</A> (pos)
</A>
    <A NAME="f_put_integer_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_32_le">put_integer_32_le</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32_le">read_integer_32_le</A> (pos)
</A>
    <A NAME="f_put_integer_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_64_le">put_integer_64_le</A> (i: <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64_le">read_integer_64_le</A> (pos)
</A>
    <A NAME="f_put_integer_8_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_8_le">put_integer_8_le</A> (i: <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8_le">read_integer_8_le</A> (pos)
</A>
    <A NAME="f_put_natural_16_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_16_le">put_natural_16_le</A> (i: <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16_le">read_natural_16_le</A> (pos)
</A>
    <A NAME="f_put_natural_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_32_le">put_natural_32_le</A> (i: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32_le">read_natural_32_le</A> (pos)
</A>
    <A NAME="f_put_natural_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_64_le">put_natural_64_le</A> (i: <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64_le">read_natural_64_le</A> (pos)
</A>
    <A NAME="f_put_natural_8_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_8_le">put_natural_8_le</A> (i: <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8_le">read_natural_8_le</A> (pos)
</A>
    <A NAME="f_put_real_32_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_32_le">put_real_32_le</A> (v: <A HREF="../base/real_32_flatshort.html">REAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`v'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: v = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_32_le">read_real_32_le</A> (pos)
</A>
    <A NAME="f_put_real_64_le"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_64_le">put_real_64_le</A> (v: <A HREF="../base/real_64_flatshort.html">REAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`v'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red"> in little-endian format.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: v = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_64_le">read_real_64_le</A> (pos)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Element change: Platform specific</FONT>

    <A NAME="f_put_array"><A HREF="../base/managed_pointer_flatshort.html#f_put_array">put_array</A> (data: <A HREF="../base/array_flatshort.html">ARRAY</A> [<A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>]; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy content of </FONT>`data'<FONT COLOR="red"> into </FONT><A HREF="../base/managed_pointer_flatshort.html#f_item">item</A><FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            data_not_void: data /= <B>Void</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + data.<A HREF="../base/array_flatshort.html#f_count">count</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: <A HREF="../base/managed_pointer_flatshort.html#f_read_array">read_array</A> (pos, data.<A HREF="../base/array_flatshort.html#f_count">count</A>).<A HREF="../base/array_flatshort.html#f_is_equal">is_equal</A> (data)
</A>
    <A NAME="f_put_boolean"><A HREF="../base/managed_pointer_flatshort.html#f_put_boolean">put_boolean</A> (b: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`b'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_boolean_bytes">boolean_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: b = <A HREF="../base/managed_pointer_flatshort.html#f_read_boolean">read_boolean</A> (pos)
</A>
    <A NAME="f_put_character"><A HREF="../base/managed_pointer_flatshort.html#f_put_character">put_character</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`c'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_character_8_bytes">character_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: c = <A HREF="../base/managed_pointer_flatshort.html#f_read_character">read_character</A> (pos)
</A>
    <A NAME="f_put_integer_16"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_16">put_integer_16</A> (i: <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_16_bytes">integer_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_16">read_integer_16</A> (pos)
</A>
    <A NAME="f_put_integer_32"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_32">put_integer_32</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_32_bytes">integer_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_32">read_integer_32</A> (pos)
</A>
    <A NAME="f_put_integer_64"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_64">put_integer_64</A> (i: <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_64_bytes">integer_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_64">read_integer_64</A> (pos)
</A>
    <A NAME="f_put_integer_8"><A HREF="../base/managed_pointer_flatshort.html#f_put_integer_8">put_integer_8</A> (i: <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_integer_8_bytes">integer_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_integer_8">read_integer_8</A> (pos)
</A>
    <A NAME="f_put_natural_16"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_16">put_natural_16</A> (i: <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_16_bytes">natural_16_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_16">read_natural_16</A> (pos)
</A>
    <A NAME="f_put_natural_32"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_32">put_natural_32</A> (i: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_32_bytes">natural_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_32">read_natural_32</A> (pos)
</A>
    <A NAME="f_put_natural_64"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_64">put_natural_64</A> (i: <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_64_bytes">natural_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_64">read_natural_64</A> (pos)
</A>
    <A NAME="f_put_natural_8"><A HREF="../base/managed_pointer_flatshort.html#f_put_natural_8">put_natural_8</A> (i: <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`i'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_natural_8_bytes">natural_8_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: i = <A HREF="../base/managed_pointer_flatshort.html#f_read_natural_8">read_natural_8</A> (pos)
</A>
    <A NAME="f_put_pointer"><A HREF="../base/managed_pointer_flatshort.html#f_put_pointer">put_pointer</A> (p: <A HREF="../base/pointer_flatshort.html">POINTER</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`p'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_pointer_bytes">pointer_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: p = <A HREF="../base/managed_pointer_flatshort.html#f_read_pointer">read_pointer</A> (pos)
</A>
    <A NAME="f_put_real_32"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_32">put_real_32</A> (r: <A HREF="../base/real_32_flatshort.html">REAL_32</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`r'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_32_bytes">real_32_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: r = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_32">read_real_32</A> (pos)
</A>
    <A NAME="f_put_real_64"><A HREF="../base/managed_pointer_flatshort.html#f_put_real_64">put_real_64</A> (d: <A HREF="../base/real_64_flatshort.html">REAL_64</A>; pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`d'<FONT COLOR="red"> at position </FONT>`pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            pos_nonnegative: pos &gt;= 0
            valid_position: (pos + <A HREF="../base/platform_flatshort.html#f_real_64_bytes">real_64_bytes</A>) &lt;= <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A>
        <B>ensure</B>
            inserted: d = <A HREF="../base/managed_pointer_flatshort.html#f_read_real_64">read_real_64</A> (pos)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Output</FONT>

    <A NAME="f_io"><A HREF="../base/any_flatshort.html#f_io">io</A>: <A HREF="../base/std_files_flatshort.html">STD_FILES</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Handle to standard file setup</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            io_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_out"><A HREF="../base/any_flatshort.html#f_out">out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New string containing terse printable representation</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            out_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_print"><A HREF="../base/any_flatshort.html#f_print">print</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Write terse external representation of </FONT>`some'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> on standard output.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_tagged_out"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_tagged_out">tagged_out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New string containing terse printable representation</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            tagged_out_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Platform</FONT>

    <A NAME="f_is_dotnet"><A HREF="../base/platform_flatshort.html#f_is_dotnet">is_dotnet</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are we targetting .NET?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_little_endian"><A HREF="../base/platform_flatshort.html#f_is_little_endian">is_little_endian</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current platform a little endian one?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_mac"><A HREF="../base/platform_flatshort.html#f_is_mac">is_mac</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are we running on Mac OS?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_thread_capable"><A HREF="../base/platform_flatshort.html#f_is_thread_capable">is_thread_capable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current platform capable of multi-threading?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_unix"><A HREF="../base/platform_flatshort.html#f_is_unix">is_unix</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are we running on a Unix like platform?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_vms"><A HREF="../base/platform_flatshort.html#f_is_vms">is_vms</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are we running on VMS?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_windows"><A HREF="../base/platform_flatshort.html#f_is_windows">is_windows</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are we running on Windows platform?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/platform_flatshort.html">PLATFORM</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_operating_environment"><A HREF="../base/any_flatshort.html#f_operating_environment">operating_environment</A>: <A HREF="../base/operating_environment_flatshort.html">OPERATING_ENVIRONMENT</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Objects available from the operating system</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            operating_environment_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Settings</FONT>

    <A NAME="f_set_from_pointer"><A HREF="../base/managed_pointer_flatshort.html#f_set_from_pointer">set_from_pointer</A> (a_ptr: <A HREF="../base/pointer_flatshort.html">POINTER</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Use directly </FONT>`a_ptr'<FONT COLOR="red"> with count </FONT>`n'<FONT COLOR="red"> to hold current data.</FONT>
        <B>require</B>
            is_shared: <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
            a_ptr_not_null: a_ptr = <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A> <B>implies</B> n = 0
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            item_set: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> = a_ptr
            count_set: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = n
            is_shared_unchanged: <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>
</A>    
<B>invariant</B>
    item_not_null: <A HREF="../base/managed_pointer_flatshort.html#f_item">item</A> = <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A> <B>implies</B> (<A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> = 0 <B>and</B> <A HREF="../base/managed_pointer_flatshort.html#f_is_shared">is_shared</A>)
    valid_count: <A HREF="../base/managed_pointer_flatshort.html#f_count">count</A> &gt;= 0

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
    reflexive_equality: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
    reflexive_conformance: <A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>)

<B>end</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">class </FONT><A HREF="../base/managed_pointer_flatshort.html">MANAGED_POINTER</A><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="managed_pointer_chart.html">Chart</A></TD><TD><A HREF="managed_pointer_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE></PRE>
<P ALIGN="CENTER"> &#045;&#045; Generated by ISE Eiffel &#045;&#045 </P>
<P ALIGN="CENTER">For more details: <A HREF="http://www.eiffel.com">www.eiffel.com</A></P>
</BODY>
</HTML>

